

@Misc{dlx,
  author = 	 {Donald E. Knuth},
  title = 	 {Dancing Links},
  note = 	 {\url{http://www-cs-faculty.stanford.edu/~uno/papers/dancing-color.ps.gz}}}



 %% hal-00778832, version 1
%% http://hal.inria.fr/hal-00778832
@inproceedings{conchon:hal-00778832,
    hal_id = {hal-00778832},
    url = {http://hal.inria.fr/hal-00778832},
    title = {{V{\'e}rification de syst{\`e}mes param{\'e}tr{\'e}s avec Cubicle}},
    author = {Conchon, Sylvain and Mebsout, Alain and Zaidi, Fatiha},
    abstract = {{Cubicle est un model-checker pour v{\'e}rifier des propri{\'e}t{\'e}s de suret{\'e} d'algorithmes faisant intervenir un nombre quelconque de processus. Ces algorithmes sont d {\'e}crits sous forme de syst{\`e}mes de transitions dits param{\`e}tres. Les propri{\'e}t{\'e}s de suret{\'e} ainsi que les {\'e}tats du syst{\`e}me sont d{\'e}crits par des formules logiques du premier ordre. Pour v{\'e}rifier ces propri{\'e}t{\'e}s, Cubicle met en oeuvre un algorithme d'atteignabilit{\'e} par cha{\^\i}nage arri{\`e}re qui utilise un d{\'e}monstrateur SMT (Satisabilit{\'e} Modulo Th{\'e}ories). Les exp{\'e}riences, men{\'e}es sur la v{\'e}rification d'algorithmes d'exclusion mutuelle et de protocoles de coh{\'e}rence de cache, montrent que Cubicle est efficace et comp{\'e}titif avec les model checkers de la m{\^e}me famille. Cubicle est un logiciel libre d {\'e}velopp{\'e} en OCaml. Il utilise le d{\'e}monstrateur Alt-Ergo zero, une version all{\'e}g{\'e}e et am{\'e}lior{\'e}e d'Alt-Ergo. Une implantation parall{\`e}le se reposant sur la biblioth{\`e}que Functory est {\'e}galement propos{\'e}e.}},
    keywords = {Cubicle;Syst{\`e}mes param{\'e}tr{\'e}s;V{\'e}rification de syst{\`e}mes param{\'e}tr{\'e}s;Model checking;Model checker symbolique},
    language = {Fran{\c c}ais},
    affiliation = {Laboratoire de Recherche en Informatique - LRI , TOCCATA - INRIA Saclay - {\^I}le-de-France},
    booktitle = {{JFLA - Journ{\'e}es francophones des langages applicatifs - 2013}},
    address = {Aussois, France},
    organization = {Damien Pous and Christine Tasson},
    editor = {Damien Pous and Christine Tasson },
    audience = {internationale },
    year = {2013},
    month = Feb,
    pdf = {http://hal.inria.fr/hal-00778832/PDF/jfla2013-02.pdf},
}


@Misc{aptkozen,
  author = 	 {Krzysztof Apt and Dexter Kozen},
  title = {{Limits for automatic verification of finite-state concurrent systems.}},
    year = {1986},
  booktitle = {{Information Processing Letters}}}



@book{tanenbaum2003systèmes,
  title={Syst{\`e}mes d'exploitation},
  author={Tanenbaum, A.},
  isbn={9782744070020},
  lccn={00051666},
  url={http://books.google.fr/books?id=IDtuPwAACAAJ},
  year={2003},
  publisher={Pearson {\'e}ducation}
}
  